COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDVAR t t1 t2 t3 t4 ε tower
C00004 ENDMK
C⊗;
declare INDVAR t t1 t2 t3 t4 ε tower;
declare INDVAR s s0 s1 s2 s3 ε situation;

declare PREDCONST movable(tower,tower,situation),on(tower,tower,situation);
declare PREDCONST reachable(situation,situation);
declare PREDPAR P 1;

axiom move:
	∀t1 t2 s.(movable(t1,t2,s) ⊃ ∃s1.(reachable(s,s1) ∧
		on(t1,t2,s1) ∧ ∀t3 t4.(¬(t3=t1) ⊃ (on(t3,t4,s1) ≡ on(t3,t4,s)))))
;;

axiom reachable:
	∀s.reachable(s,s)
	∀s1 s2 s3.(reachable(s1,s2) ∧ reachable(s2,s3) ⊃ reachable(s1,s3))
BIG PROBLEM IN FIXING THE INDUCTION AXIOM WITHOUT THE FUNCTIONS
	∀s0.(P(s0) ∧ ∀s t1 t2.(P(s) ∧ movable(t1,t2,s) ⊃ P(move(t1,t2,s)))
				⊃ ∀s.(reachable(s0,s) ⊃ P(s)))
;;